VERS5 
NIL 
((LISTINDUCTION LISPAX#30) (LISTINDUCTIONDEF LISPAX#34) (SEXPINDUCTION LISPAX#35) (SEXPINDUCTIONDEF LISPAX#36) (HIGH_ORDER_DEFINITION LISPAX#40) (LISTDEF LISPAX#45) (APPENDEF LISPAX#47) (LISTAPPEND LISPAX#48) (ALLPDEF LISPAX#52) (SOMEPDEF LISPAX#53) (MAPCARDEF LISPAX#54) (ALISTDEF1 LISPAX#57) (ALISTDEF LISPAX#58) (ASSOCDEF LISPAX#60) (MEMBERDEF LISPAX#63) (UNIQUENESSDEF LISPAX#65) (ALLPFACT ALLP#1) (ALLP_INTRODUCTION ALLP#2) (ALLP_ELIMINATION ALLP#3) (ALLP_IMPLICATION ALLP#4) (SOMEPFACT ALLP#5) (EPSILONDEF SETS#6) (SET_EXTENSIONALITY SETS#7) (INTERDEF SETS#9) (UNIONDEF SETS#11) (INCLUSIONDEF SETS#13) (MKSET_DEF SETS#17) (MKLSETDEF SETS#19) (MKSET_MKLSET SETFACTS#1) (DOUBLE_INCLUSION SETFACTS#2) (DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (IRREFLEXIVITY_OF_ORDER NATNUM#7) (TRANSITIVITY_OF_ORDER NATNUM#8) (ZEROLEAST1 NATNUM#9) (SUCCESSOR1 NATNUM#11) (SUCCESSOR2 NATNUM#12) (SUCCESSORLESS NATNUM#13) (SUCCESSOREQ NATNUM#14) (ZEROLEAST2 NATNUM#15) (ZEROLEAST3 NATNUM#16) (ZERO_NOT_SUCCESSOR NATNUM#17) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (COMMUTADD NATNUM#29) (TIMSUCC NATNUM#33) (LTIMESCAN NATNUM#34) (RTIMESCAN NATNUM#35) (COMMUTMULT NATNUM#36) (LTIMESTOZERO NATNUM#37) (RTIMESTOZERO NATNUM#38) (LDISTRIB NATNUM#39) (RDISTRIB NATNUM#40) (PROOF_BY_INDUCTION INDUCTION#1) (INDUCTIVE_DEFINITION INDUCTION#5) (PROOF_BY_DOUBLEINDUCTION INDUCTION#6) (HIGH_ORDER_NATNUM_DEFINITION INDUCTION#10) (INFINITE_DESCENT INDUCTION#11) (LESSEQDEF LESSEQ#3) (SUCCESSORLESSEQ LESSEQ#4) (SUCCESSORFACTS LESSEQ#4) (TRANS_LESSEQ LESSEQ#5) (LESS_LESSEQ_FACT1 LESSEQ#6) (ZEROLEAST LESSEQ#7) (ONELEASTSUCC LESSEQ#8) (ZERO_NON_LESS_SUCCESSOR LESSEQ#9) (SUCC_LESS_LESS LESSEQ#10) (SUCC_LESSEQ_LESSEQ LESSEQ#11) (LESSEQ_LESSEQ_SUCC LESSEQ#12) (LESS_SUCC_LESSEQ LESSEQ#13) (LESS_LESSEQSUCC LESSEQ#14) (LEQ_LEQ_EQ LESSEQ#15) (TRICHOTOMY LESSEQ#16) (MINUSDEF MINUS#2) (MINUS_SORT MINUS#3) (MINUSFACT3 MINUS#4) (MINUSFACT5 MINUS#5) (SUCCESSOR_MINUS MINUS#6) (MINUSFACT10 MINUS#7) (MINUSFACT11 MINUS#8) (N_LESS_N MINUS#9) (MINUS1 MINUS#10) (TOTAL_SUBTRACTION MINUS#11) (INEQUALITY_LAW MINUS#12) (ADD_LESSEQ MINUS#13) (ADD_ONE MINUS#14) (LENGTHDEF LENGTH#2) (LENGTHADD LENGTH#5) (TRICHOTOMY2 LENGTH#7) (HAVE_MEMBER LENGTH#8) (HAVE_MEMBER1 LENGTH#9) (DOUBLEINDUCTION LISTINDUCTION#1) (DOUBLEINDUCTION1 LISTINDUCTION#2) (NTHDEF NTH#2) (SEXP_NTH NTH#3) (NTHMEMBER NTH#4) (MEMBER_NTH NTH#5) (NTHCDRDEF NTHCDR#2) (NTH_NTHCDR_ZERO NTHCDR#4) (CAR_NTHCDR NTHCDR#5) (CDR_NTHCDR NTHCDR#6) (NTHCDR_CAR_CDR NTHCDR#7) (NTH_IN_NTHCDR NTHCDR#8) (NTH_NTHCDR NTHCDR#9) (LENGTH_NTHCDR NTHCDR#10) (LAST_NTHCDR NTHCDR#11) (TRIVIAL_NTHCDR NTHCDR#12) (ALLP_NTHCDR NTHCDR#13) (NTHCDR_INDUCTION1 NTHCDR#14) (NTHCDR_INDUCTION NTHCDR#15) (FSTPOSITIONDEF FSTPOSITION#2) (POSFACTS FSTPOSITION#3) (SORTPOS FSTPOSITION#4) (POS_LENGTH FSTPOSITION#5) (NTH_FSTPOSITION FSTPOSITION#6) (FSTPOSITION_NTH FSTPOSITION#7) (INJDEF INJ#2) (UNIQUENESS_INJECTIVITY INJ#3) (NTH_ALLP ALLP#6) (MKLSET_FACT SETFACTS#3) (DOMDEF APPALIST#2) (RANGEDEF APPALIST#4) (FUNCTDEF APPALIST#6) (INJECTDEF APPALIST#8) (APPALISTDEF APPALIST#10) (SAMEMAPDEF APPALIST#12) (PERMUTP_DEF APPALIST#13) (ALISTINDUCTION APPALIST#14) (DOMSORT ALISTFACTS#1) (RANGESORT ALISTFACTS#2) (DOMLENGTH ALISTFACTS#3) (DOMRANGELENGTH ALISTFACTS#4) (APPALISTSORT ALISTFACTS#5) (TRIVIAL_APPALIST ALISTFACTS#6) (SAMEMAP_DEF1 ALISTFACTS#10) (APPLDEF APPL#1) (EXTENSIONALITY APPL#2) (APPLFACTS APPL#3) (INTODEF APPL#5) (ONTODEF APPL#7) (ALLNUMDEF SUMS#7) (SOMENUMDEF SUMS#8) (SUMDEF SUMS#9) (UNDEF SUMS#10) (DISJPAIR_DEF SUMS#12) (DISJOINTDEF SUMS#14) (ALLNUMFACT SUMFACTS#1) (SOMENUMFACT SUMFACTS#2) (UNIONFACT1 SUMFACTS#3) (MKSETFACT SUMFACTS#4) (MKLSET_UN SUMFACTS#5) (SUMSORT SUMFACTS#6) (MULT_DEF MULTIPLICITY#2) (MULTFACT MULTIPLICITY#3) (LENGTH_MULT MULTIPLICITY#4) (MEMBER_MULT MULTIPLICITY#5) (MULT_NTHCDR MULTIPLICITY#6) (EMPTYFACTS MULTIPLICITY#7) (MULTINJ_COMPUTATION MULTIPLICITY#8) (MULT_INJ MULTIPLICITY#9) (MULTSUM MULT_OF_UN_IS_SUM_UN#1) (MULT_OF_UN_IS_SUM_MULT MULT_OF_UN_IS_SUM_UN#2) (CONS_CAR_CDR LISPAX#28 LISPAX#29) (SAMEMAP_EQUIVALENCE ALISTFACTS#7 ALISTFACTS#8 ALISTFACTS#9) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (SUCCFACTS NATNUM#11 NATNUM#12 NATNUM#13 NATNUM#14 NATNUM#15 NATNUM#16 NATNUM#17) (TIMESFACTS NATNUM#30 NATNUM#32 NATNUM#33 NATNUM#34 NATNUM#35 NATNUM#36 NATNUM#37 NATNUM#38 NATNUM#39 NATNUM#40) (PLUSFACTS NATNUM#21 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 NATNUM#29 NATNUM#39 NATNUM#40) (SIMPINFO LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5 APPL#3 MULTIPLICITY#3 MULTIPLICITY#7)) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (XV YV ZV) (TYPE: (TY& . GROUND)) (SORT: (TM& . URELEMENT))) . ((ZV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (YV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (XV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (URELEMENT . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (AV BV) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((BV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (AV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(|∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R|)) . ((R . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (Q . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . NATNUM#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 5 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 6 .)(NIL . (DECL MINUS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (INFIXNAME: -) (BINDINGPOWER: 940)) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . MINUS . NIL . 1 .)(NIL . (DECL LENGTH (TYPE: (TY& . GROUND→GROUND)) (UNARYNAME: LENGTH)) . ((LENGTH . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((UNARY& . LENGTH)) . LENGTH#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . LENGTH . NIL . 1 .)(NIL . (DECL NTH (SYNTYPE: CONSTANT) (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|))) . ((NTH . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NTH#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NTH . NIL . 1 .)(NIL . (DECL NTHCDR (SYNTYPE: CONSTANT) (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|))) . ((NTHCDR . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NTHCDR#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NTHCDR . NIL . 1 .)(NIL . (DECL (FSTPOSITION) (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|))) . ((FSTPOSITION . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FSTPOSITION#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . FSTPOSITION . NIL . 1 .)(NIL . (DECL (INJ) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((INJ . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INJ#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . INJ . NIL . 1 .)(NIL . (DECL DOM (TYPE: (TY& . GROUND→GROUND))) . ((DOM . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 1 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(|∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q|)) . (R Q P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R|)) . (R Q P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)| . (AXIOM (TM& . |∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)|)) . (R Q P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P Q.¬(P∨Q)≡¬P∧¬Q| . (AXIOM (TM& . |∀P Q.¬(P∨Q)≡¬P∧¬Q|)) . (R Q P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P Q.¬(P∧Q)≡¬P∨¬Q| . (AXIOM (TM& . |∀P Q.¬(P∧Q)≡¬P∨¬Q|)) . (R Q P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P Q.P≡(Q⊃P)∧(¬Q⊃P)| . (AXIOM (TM& . |∀P Q.P≡(Q⊃P)∧(¬Q⊃P)|)) . (R Q P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R| . (DERIVE (TM& . |∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R|) ((LR&)) NIL) . (R Q P) . NIL . NIL . NIL . NORMAL . NIL . 8 .)(|∀N.¬N<N| . (AXIOM (TM& . |∀N.¬N<N|)) . (LESSP M N K J I) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (LESSP M N K J I) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (LESSP M N K J I) . NIL . (NATNUM#9) . NIL . NATNUM . NIL . 9 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (ADD1 M N K J I) . NIL . (NATNUM#10) . NIL . NATNUM . NIL . 10 .)(|∀N.N<N'| . (AXIOM (TM& . |∀N.N<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#11) . NIL . NATNUM . NIL . 11 .)(|∀N M.¬N<M⊃M<N'| . (AXIOM (TM& . |∀N M.¬N<M⊃M<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#12) . NIL . NATNUM . NIL . 12 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (ADD1 M N K J I) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (LESSP M N K J I) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.0<N'| . (AXIOM (TM& . |∀N.0<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (ADD1 M N K J I) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(NIL . (DECL PRED (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#18 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 18 .)(|∀N.PRED(N')=N| . (DEFAX PRED (TM& . |∀N.PRED(N')=N|)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#19 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (ADD1 M N K J I SET C B (A . NATNUM#6)) . NIL . (INDUCTION#1) . NIL . INDUCTION . NIL . 1 .)(NIL . (DECL NPARS (TYPE: (TY& . GROUND*))) . ((NPARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 2 .)(NIL . (DECL NDF (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((NDF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 3 .)(NIL . (DECL ZCASE (TYPE: (TY& . |(GROUND*)→GROUND|))) . ((ZCASE . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 4 .)(|∀N.¬N=N'| . (AXIOM (TM& . |∀N.¬N=N'|)) . (ADD1 M N K J I) . NIL . (LESSEQ#1) . NIL . LESSEQ . NIL . 1 .)(NIL . (DECL LESSEQ (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . LESSEQ . NIL . 2 .)(NIL . (DECL ALLNUM (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((ALLNUM . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 1 .)(NIL . (DECL SOMENUM (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((SOMENUM . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#2 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 2 .)(NIL . (DECL (NUMSEQ F) (TYPE: (TY& . GROUND→GROUND))) . ((F . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#3 . NIL . VARIABLE .)) (NUMSEQ . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . SUMS . NIL . 3 .)(NIL . (DECL MULT (TYPE: (TY& . |(GROUND⊗(@SET))→GROUND|)) (SYNTYPE: CONSTANT)) . ((MULT . (|(GROUND⊗(@SET))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MULTIPLICITY#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . MULTIPLICITY . NIL . 1 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|CAR NIL=NIL| . (AXIOM (TM& . |CAR NIL=NIL|)) . (CAR) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|CDR NIL=NIL| . (AXIOM (TM& . |CDR NIL=NIL|)) . (CDR) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#29) . NIL . LISPAX . NIL . 29 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30) . NIL . LISPAX . NIL . 30 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 32 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 33 .)(|∀X.URELEMENT(X)| . (AXIOM (TM& . |∀X.URELEMENT(X)|)) . (SEXP Z Y X URELEMENT ZV YV XV) . NIL . (SETS#3) . NIL . SETS . NIL . 3 .)(|∀XV.SEXP XV| . (AXIOM (TM& . |∀XV.SEXP XV|)) . (SEXP URELEMENT ZV YV XV) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(NIL . (DECL EPSILON (TYPE: (TY& . |(GROUND⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#5 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 5 .)(|∀N.NATNUM(PRED(N))| . (AXIOM (TM& . |∀N.NATNUM(PRED(N))|)) . (ADD1 M N K J I PRED) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#21 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀X U N.NTH(NIL,N)=NIL∧NTH(U,0)=CAR U∧NTH(X.U,N')=NTH(U,N)| . (DEFAX NTH (TM& . |∀X U N.NTH(NIL,N)=NIL∧NTH(U,0)=CAR U∧NTH(X.U,N')=NTH(U,N)|)) . ((NTH . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NTH#2 . NIL . DEFINED .)) CAR LISTP SEXP ADD1 M N K J I W V U Z Y X CONS) . NIL . (NTH#2) . NIL . NTH . NIL . 2 .)(|∀X U N.NTHCDR(NIL,N)=NIL∧NTHCDR(U,0)=U∧NTHCDR(X.U,N')=NTHCDR(U,N)| . (DEFAX NTHCDR (TM& . |∀X U N.NTHCDR(NIL,N)=NIL∧NTHCDR(U,0)=U∧NTHCDR(X.U,N')=NTHCDR(U,N)|)) . ((NTHCDR . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NTHCDR#2 . NIL . DEFINED .)) LISTP SEXP ADD1 M N K J I W V U Z Y X CONS) . NIL . (NTHCDR#2) . NIL . NTHCDR . NIL . 2 .)(|∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))| . (AXIOM (TM& . |∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))|)) . (ADD1 M N K J I NPARS NDF ZCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .)) (NDEF . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .))) . NIL . (INDUCTION#5) . NIL . INDUCTION . NIL . 5 .)(|∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))| . (AXIOM (TM& . |∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))|)) . (ADD1 M N K J I (A2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#6 . NIL . VARIABLE .))) . NIL . (INDUCTION#6) . NIL . INDUCTION . NIL . 6 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 7 .)(NIL . (DECL SUM (TYPE: (TY& . |((@NUMSEQ)⊗(@N))→(@N)|)) (SYNTYPE: CONSTANT)) . ((SUM . (|((@NUMSEQ)⊗(@N))→(@N)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#4 . NIL . CONSTANT .)) N NUMSEQ) . NIL . NIL . NIL . SUMS . NIL . 4 .)(NIL . (DECL SETSEQ (TYPE: (TY& . |(@N)→(@SET)|))) . ((SETSEQ . (|(@N)→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#5 . NIL . VARIABLE .)) SET N) . NIL . NIL . NIL . SUMS . NIL . 5 .)(|∀PHI2.(∀U V X Y.PHI2(NIL,U)∧PHI2(U,NIL)∧(PHI2(U,V)⊃PHI2(X.U,Y.V)))⊃ (∀U V.PHI2(U,V))| . (AXIOM (TM& . |∀PHI2.(∀U V X Y.PHI2(NIL,U)∧PHI2(U,NIL)∧(PHI2(U,V)⊃PHI2(X.U,Y.V)))⊃ (∀U V.PHI2(U,V))|)) . (LISTP SEXP W V U Z Y X CONS (PHI2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISTINDUCTION#1 . NIL . VARIABLE .))) . NIL . (LISTINDUCTION#1) . NIL . LISTINDUCTION . NIL . 1 .)(|∀PHI3.(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))| . (AXIOM (TM& . |∀PHI3.(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))|)) . (LISTP SEXP ADD1 M N K J I W V U Z Y X CONS (PHI3 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISTINDUCTION#2 . NIL . VARIABLE .))) . NIL . (LISTINDUCTION#2) . NIL . LISTINDUCTION . NIL . 2 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#35) . NIL . LISPAX . NIL . 35 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#29) . NIL . NATNUM . NIL . 29 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#30 . NIL . DEFINED .)) ADD1 PLUS M N K J I) . NIL . (NATNUM#30) . NIL . NATNUM . NIL . 30 .)(|∀U N.SEXP NTH(U,N)| . (AXIOM (TM& . |∀U N.SEXP NTH(U,N)|)) . (CAR LISTP SEXP ADD1 M N K J I W V U Z Y X CONS NTH) . NIL . (NTH#3) . NIL . NTH . NIL . 3 .)(|∀U N.LISTP NTHCDR(U,N)| . (AXIOM (TM& . |∀U N.LISTP NTHCDR(U,N)|)) . (LISTP SEXP ADD1 M N K J I W V U Z Y X CONS NTHCDR) . NIL . (NTHCDR#3) . NIL . NTHCDR . NIL . 3 .)(NIL . (DECL INDFN (TYPE: (TY& . |(GROUND⊗(@ARB))→(@ARB)|))) . ((INDFN . (|(GROUND⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#8 . NIL . VARIABLE .)) (ARB . INDUCTION#7)) . NIL . NIL . NIL . INDUCTION . NIL . 8 .)(NIL . (DECL (DEF_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((DEF_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#9 . NIL . VARIABLE .)) (ARB . INDUCTION#7)) . NIL . NIL . NIL . INDUCTION . NIL . 9 .)(NIL . (DECL UN (TYPE: (TY& . |((@SETSEQ)⊗(@N))→(@SET)|)) (SYNTYPE: CONSTANT)) . ((UN . (|((@SETSEQ)⊗(@N))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#6 . NIL . CONSTANT .)) SET N SETSEQ) . NIL . NIL . NIL . SUMS . NIL . 6 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .))) . NIL . (LISPAX#36) . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|∀N M.NATNUM(M*N)| . (AXIOM (TM& . |∀N M.NATNUM(M*N)|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#31) . NIL . NATNUM . NIL . 31 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#32) . NIL . NATNUM . NIL . 32 .)(|∀N K.N*K'=N*K+N| . (AXIOM (TM& . |∀N K.N*K'=N*K+N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#33) . NIL . NATNUM . NIL . 33 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#34) . NIL . NATNUM . NIL . 34 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#35) . NIL . NATNUM . NIL . 35 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#36) . NIL . NATNUM . NIL . 36 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#37) . NIL . NATNUM . NIL . 37 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#38) . NIL . NATNUM . NIL . 38 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#39) . NIL . NATNUM . NIL . 39 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#40) . NIL . NATNUM . NIL . 40 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#38 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 38 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(|∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))| . (AXIOM (TM& . |∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))|)) . (ADD1 M N K J I ARB2 ARB1 ARB INDFN DEF_FUN) . NIL . (INDUCTION#10) . NIL . INDUCTION . NIL . 10 .)(|¬(∃DESC.(∀N.DESC(N')<DESC(N)))| . (AXIOM (TM& . |¬(∃DESC.(∀N.DESC(N')<DESC(N)))|)) . (LESSP ADD1 M N K J I (DESC . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#11 . NIL . VARIABLE .))) . NIL . (INDUCTION#11) . NIL . INDUCTION . NIL . 11 .)(|∀M N.M≤N=(M=N∨M<N)| . (DEFINE LESSEQ (TM& . |∀M N.M≤N=(M=N∨M<N)|) NIL) . ((LESSEQ . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . LESSEQ#3 . NIL . DEFINED .)) LESSP M N K J I) . NIL . (LESSEQ#3 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1) . NIL . LESSEQ . NIL . 3 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS ARB BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#40) . NIL . LISPAX . NIL . 40 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#41 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 41 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#42 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 42 .)(|∀N M.N'≤M'≡N≤M| . (AXIOM (TM& . |∀N M.N'≤M'≡N≤M|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#4) . NIL . LESSEQ . NIL . 4 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#5) . NIL . LESSEQ . NIL . 5 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#6) . NIL . LESSEQ . NIL . 6 .)(|∀N.0≤N| . (AXIOM (TM& . |∀N.0≤N|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#7) . NIL . LESSEQ . NIL . 7 .)(|∀N.1≤N'| . (AXIOM (TM& . |∀N.1≤N'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#8) . NIL . LESSEQ . NIL . 8 .)(|∀N M.N'<M⊃¬M=0| . (AXIOM (TM& . |∀N M.N'<M⊃¬M=0|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#9) . NIL . LESSEQ . NIL . 9 .)(|∀M N.M'<N⊃M<N| . (AXIOM (TM& . |∀M N.M'<N⊃M<N|)) . (LESSP ADD1 M N K J I) . NIL . (LESSEQ#10) . NIL . LESSEQ . NIL . 10 .)(|∀M N.M'≤N⊃M≤N| . (AXIOM (TM& . |∀M N.M'≤N⊃M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#11) . NIL . LESSEQ . NIL . 11 .)(|∀N M.N≤M⊃N≤M'| . (AXIOM (TM& . |∀N M.N≤M⊃N≤M'|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#12) . NIL . LESSEQ . NIL . 12 .)(|∀N M.M<N'≡M≤N| . (AXIOM (TM& . |∀N M.M<N'≡M≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#13) . NIL . LESSEQ . NIL . 13 .)(|∀M N.M<N=M'≤N| . (AXIOM (TM& . |∀M N.M<N=M'≤N|)) . (LESSP ADD1 M N K J I LESSEQ) . NIL . (LESSEQ#14) . NIL . LESSEQ . NIL . 14 .)(|∀N M.N≤M∧M≤N⊃N=M| . (AXIOM (TM& . |∀N M.N≤M∧M≤N⊃N=M|)) . (LESSP M N K J I LESSEQ) . NIL . (LESSEQ#15) . NIL . LESSEQ . NIL . 15 .)(|∀N M.M<N∨M=N∨N<M| . (AXIOM (TM& . |∀N M.M<N∨M=N∨N<M|)) . (LESSP M N K J I) . NIL . (LESSEQ#16) . NIL . LESSEQ . NIL . 16 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#44) . NIL . LISPAX . NIL . 44 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#46 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 46 .)(|∀X U V.NIL*V=V∧X.U*V=X.(U*V)| . (DEFAX APPEND (TM& . |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#47 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀M N.M-0=M∧M-N'=PRED(M-N)| . (DEFINE MINUS (TM& . |∀M N.M-0=M∧M-N'=PRED(M-N)|) (USE (LR& INDUCTION#5))) . ((MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940) (INFIX& . -)) . MINUS#2 . NIL . DEFINED .)) ADD1 M N K J I PRED) . NIL . (MINUS#2 INDUCTION#5 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9) . NIL . MINUS . NIL . 2 .)(|∀U V.LISTP U*V| . (AXIOM (TM& . |∀U V.LISTP U*V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(|∀U.U*NIL=U| . (AXIOM (TM& . |∀U.U*NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#49) . NIL . LISPAX . NIL . 49 .)(|∀X V.X.NIL*V=X.V| . (AXIOM (TM& . |∀X V.X.NIL*V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 51 .)(|∀N K.NATNUM(K-N)| . (AXIOM (TM& . |∀N K.NATNUM(K-N)|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#3) . NIL . MINUS . NIL . 3 .)(|∀N M.N<M⊃0<M-N| . (AXIOM (TM& . |∀N M.N<M⊃0<M-N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#4) . NIL . MINUS . NIL . 4 .)(|∀N.0<N⊃PRED(N)'=N| . (AXIOM (TM& . |∀N.0<N⊃PRED(N)'=N|)) . (LESSP ADD1 M N K J I PRED) . NIL . (MINUS#5) . NIL . MINUS . NIL . 5 .)(|∀N M.N≤M⊃M'-N=(M-N)'| . (AXIOM (TM& . |∀N M.N≤M⊃M'-N=(M-N)'|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#6) . NIL . MINUS . NIL . 6 .)(|∀N M.N<M⊃M-N=(M-N')'| . (AXIOM (TM& . |∀N M.N<M⊃M-N=(M-N')'|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#7) . NIL . MINUS . NIL . 7 .)(|∀N M.M<N⊃N-M'<N| . (AXIOM (TM& . |∀N M.M<N⊃N-M'<N|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#8) . NIL . MINUS . NIL . 8 .)(|∀N.N-N=0| . (AXIOM (TM& . |∀N.N-N=0|)) . (ADD1 M N K J I PRED MINUS) . NIL . (MINUS#9) . NIL . MINUS . NIL . 9 .)(|∀N.0<N⊃N-PRED(N)=1| . (AXIOM (TM& . |∀N.0<N⊃N-PRED(N)=1|)) . (LESSP ADD1 M N K J I PRED MINUS) . NIL . (MINUS#10) . NIL . MINUS . NIL . 10 .)(|∀N M.M≤N⊃M-N=0| . (AXIOM (TM& . |∀N M.M≤N⊃M-N=0|)) . (LESSP ADD1 M N K J I PRED LESSEQ MINUS) . NIL . (MINUS#11) . NIL . MINUS . NIL . 11 .)(|∀N M K.K<N∧M<N-K≡M+K<N| . (AXIOM (TM& . |∀N M K.K<N∧M<N-K≡M+K<N|)) . (LESSP ADD1 PLUS M N K J I PRED MINUS) . NIL . (MINUS#12) . NIL . MINUS . NIL . 12 .)(|∀N K M.N≤M∧1≤K⊃N'≤M+K| . (AXIOM (TM& . |∀N K M.N≤M∧1≤K⊃N'≤M+K|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#13) . NIL . MINUS . NIL . 13 .)(|∀K N M.1≤K∧M+K=N'∧N≤M⊃1=K∧N=M| . (AXIOM (TM& . |∀K N M.1≤K∧M+K=N'∧N≤M⊃1=K∧N=M|)) . (LESSP ADD1 PLUS M N K J I LESSEQ) . NIL . (MINUS#14) . NIL . MINUS . NIL . 14 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#51)) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#53 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#53) . NIL . LISPAX . NIL . 53 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . VARIABLE .))) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#55 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 55 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(|∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)| . (AXIOM (TM& . |∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)|)) . (CAR CDR ATOM NULL LISTP ALISTP W V U) . NIL . (LISPAX#57) . NIL . LISPAX . NIL . 57 .)(|∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#59 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 59 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#60) . NIL . LISPAX . NIL . 60 .)(|∀XA Y ALIST.DOM(NIL)=NIL∧DOM((XA.Y).ALIST)=XA.DOM(ALIST)| . (DEFAX DOM (TM& . |∀XA Y ALIST.DOM(NIL)=NIL∧DOM((XA.Y).ALIST)=XA.DOM(ALIST)|)) . ((DOM . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#2 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (APPALIST#2) . NIL . APPALIST . NIL . 2 .)(NIL . (DECL RANGE (TYPE: (TY& . GROUND→GROUND))) . ((RANGE . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 3 .)(|∀XA Y ALIST.RANGE(NIL)=NIL∧RANGE((XA.Y).ALIST)=Y.RANGE(ALIST)| . (DEFAX RANGE (TM& . |∀XA Y ALIST.RANGE(NIL)=NIL∧RANGE((XA.Y).ALIST)=Y.RANGE(ALIST)|)) . ((RANGE . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#4 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (APPALIST#4) . NIL . APPALIST . NIL . 4 .)(NIL . (DECL FUNCTP (TYPE: (TY& . GROUND→TRUTHVAL))) . ((FUNCTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 5 .)(|∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)| . (AXIOM (TM& . |∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP) . NIL . (ALLP#1) . NIL . ALLP . NIL . 1 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#62 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 62 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#63 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#63) . NIL . LISPAX . NIL . 63 .)(NIL . (DECL UNIQUENESS (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#64 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 64 .)(|∀ALIST.LISTP DOM(ALIST)| . (AXIOM (TM& . |∀ALIST.LISTP DOM(ALIST)|)) . (ATOM LISTP ALISTP SEXP Z Y X ZA YA XA CONS ALIST DOM) . NIL . (ALISTFACTS#1) . NIL . ALISTFACTS . NIL . 1 .)(|∀ALIST.LISTP RANGE(ALIST)| . (AXIOM (TM& . |∀ALIST.LISTP RANGE(ALIST)|)) . (ATOM LISTP ALISTP SEXP Z Y X ZA YA XA CONS ALIST RANGE) . NIL . (ALISTFACTS#2) . NIL . ALISTFACTS . NIL . 2 .)(|∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))| . (DEFAX UNIQUENESS (TM& . |∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))|)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#65 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS MEMBER) . NIL . (LISPAX#65) . NIL . LISPAX . NIL . 65 .)(|∀U.SEXP CAR U| . (UE (UELST& (PHI . |λU.SEXP CAR U|)) (LN& . LISPAX#30) NIL) . (CAR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61) . NIL . LISPAX . NIL . 66 .)(|∀PHI1 U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)| . (AXIOM (TM& . |∀PHI1 U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP MEMBER (PHI1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . ALLP#2 . NIL . VARIABLE .))) . NIL . (ALLP#2) . NIL . ALLP . NIL . 2 .)(|∀U.LISTP CDR U| . (UE (UELST& (PHI . |λU.LISTP CDR U|)) (LN& . LISPAX#30) NIL) . (CDR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66) . NIL . LISPAX . NIL . 67 .)(|∀N.SEXP N| . (AXIOM (TM& . |∀N.SEXP N|)) . (SEXP M N K J I) . NIL . (LISPAX#68) . NIL . LISPAX . NIL . 68 .)(|∀N.¬NULL N| . (AXIOM (TM& . |∀N.¬NULL N|)) . (NULL M N K J I) . NIL . (LISPAX#69) . NIL . LISPAX . NIL . 69 .)(|∀PHI1 X U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)| . (AXIOM (TM& . |∀PHI1 X U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP MEMBER PHI1) . NIL . (ALLP#3) . NIL . ALLP . NIL . 3 .)(|∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)| . (AXIOM (TM& . |∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP (A1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALLP#4 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALLP#4 . NIL . VARIABLE .))) . NIL . (ALLP#4) . NIL . ALLP . NIL . 4 .)(|∀PHI1 U.SOMEP(PHI1,U)≡(∃X.MEMBER(X,U)∧PHI1(X))| . (AXIOM (TM& . |∀PHI1 U.SOMEP(PHI1,U)≡(∃X.MEMBER(X,U)∧PHI1(X))|)) . (LISTP SEXP W V U Z Y X PHI CONS SOMEP ALLP MEMBER PHI1) . NIL . (ALLP#5) . NIL . ALLP . NIL . 5 .)(|∀AV XV.XVεAV≡AV(XV)| . (DEFINE EPSILON (TM& . |∀AV XV.XVεAV≡AV(XV)|) NIL) . ((EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#6 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#6 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 6 .)(|∀U X.LENGTH NIL=0∧LENGTH (X.U)=LENGTH U'| . (DEFINE LENGTH (TM& . |∀U X.LENGTH NIL=0∧LENGTH (X.U)=LENGTH U'|) (USE (LR& LISPAX#34))) . ((LENGTH . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((UNARY& . LENGTH)) . LENGTH#2 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS ADD1) . NIL . (LENGTH#2 LISPAX#30 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9) . NIL . LENGTH . NIL . 2 .)(|∀N A.ALLNUM(0,A)∧(ALLNUM(N',A)≡A(N)∧ALLNUM(N,A))| . (DEFAX ALLNUM (TM& . |∀N A.ALLNUM(0,A)∧(ALLNUM(N',A)≡A(N)∧ALLNUM(N,A))|)) . ((ALLNUM . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#7 . NIL . DEFINED .)) LISTP SEXP ADD1 M N K J I SET A W V U Z Y X PHI CONS ALLP A1) . NIL . (SUMS#7) . NIL . SUMS . NIL . 7 .)(|∀N A.¬SOMENUM(0,A)∧(SOMENUM(N',A)≡A(N)∨SOMENUM(N,A))| . (DEFAX SOMENUM (TM& . |∀N A.¬SOMENUM(0,A)∧(SOMENUM(N',A)≡A(N)∨SOMENUM(N,A))|)) . ((SOMENUM . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#8 . NIL . DEFINED .)) LISTP SEXP ADD1 M N K J I SET A W V U Z Y X PHI CONS ALLP A1) . NIL . (SUMS#8) . NIL . SUMS . NIL . 8 .)(|∀N NUMSEQ.SUM(NUMSEQ,0)=0∧SUM(NUMSEQ,N')=SUM(NUMSEQ,N)+NUMSEQ(N)| . (DEFAX SUM (TM& . |∀N NUMSEQ.SUM(NUMSEQ,0)=0∧SUM(NUMSEQ,N')=SUM(NUMSEQ,N)+NUMSEQ(N)|)) . ((SUM . (|((@NUMSEQ)⊗(@N))→(@N)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#9 . NIL . DEFINED .)) ADD1 PLUS M N K J I F NUMSEQ) . NIL . (SUMS#9) . NIL . SUMS . NIL . 9 .)(|∀X U A.MULT(NIL,A)=0∧MULT(X.U,A)=(IF A(X) THEN MULT(U,A)' ELSE MULT(U,A))| . (DEFAX MULT (TM& . |∀X U A.MULT(NIL,A)=0∧MULT(X.U,A)=(IF A(X) THEN MULT(U,A)' ELSE MULT(U,A))|)) . (LISTP SEXP ADD1 SET A W V U Z Y X PHI CONS ALLP A1 (MULT . (|(GROUND⊗(@SET))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MULTIPLICITY#2 . NIL . DEFINED .))) . NIL . (MULTIPLICITY#2) . NIL . MULTIPLICITY . NIL . 2 .)(|∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV| . (AXIOM (TM& . |∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV EPSILON) . NIL . (SETS#7) . NIL . SETS . NIL . 7 .)(NIL . (DECL INTERSECTION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∩) (BINDINGPOWER: 950) (PREFIXNAME: INTERSECTION)) . ((INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#8 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))| . (DEFINE INTERSECTION (TM& . |∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))|) NIL) . ((INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#9 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#9 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 9 .)(NIL . (DECL UNION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∪) (BINDINGPOWER: 950) (PREFIXNAME: UNION)) . ((UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#10 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 10 .)(|∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))| . (DEFINE UNION (TM& . |∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))|) NIL) . ((UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#11 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#11 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 11 .)(NIL . (DECL INCLUSION (TYPE: (TY& . |((@AV)⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ⊂) (BINDINGPOWER: 920) (PREFIXNAME: INCLUSION)) . ((INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#12 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 12 .)(|∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))| . (DEFINE INCLUSION (TM& . |∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))|) NIL) . ((INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#13 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#13 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 13 .)(|EMPTYSET=(λXV.FALSE)| . (DEFAX EMPTYSET (TM& . |EMPTYSET=(λXV.FALSE)|)) . ((EMPTYSET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#14 . NIL . DEFINED .)) URELEMENT ZV YV XV) . NIL . (SETS#14) . NIL . SETS . NIL . 14 .)(|∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))| . (DEFAX EMPTYP (TM& . |∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))|)) . ((EMPTYP . (|(GROUND→TRUTHVAL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#15 . NIL . DEFINED .)) URELEMENT ZV YV XV BV AV) . NIL . (SETS#15) . NIL . SETS . NIL . 15 .)(NIL . (DECL MKSET (TYPE: (TY& . |GROUND→(@AV)|))) . ((MKSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#16 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 16 .)(|∀X.MKSET(X)=(λYV.YV=X)| . (DEFINE MKSET (TM& . |∀X.MKSET(X)=(λYV.YV=X)|) NIL) . ((MKSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#17 . NIL . DEFINED .)) SEXP Z Y X URELEMENT ZV YV XV AV) . NIL . (SETS#17 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 17 .)(NIL . (DECL MKLSET (TYPE: (TY& . |GROUND→(@AV)|))) . ((MKLSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#18 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 18 .)(|∀U.MKLSET(U)=(λX.MEMBER(X,U))| . (DEFINE MKLSET (TM& . |∀U.MKLSET(U)=(λX.MEMBER(X,U))|) NIL) . ((MKLSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#19 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS MEMBER AV) . NIL . (SETS#19 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 19 .)(|∀N.URELEMENT(N)| . (AXIOM (TM& . |∀N.URELEMENT(N)|)) . (ZV YV XV URELEMENT M N K J I) . NIL . (SETS#20) . NIL . SETS . NIL . 20 .)(|∀U.NATNUM(LENGTH U)| . (AXIOM (TM& . |∀U.NATNUM(LENGTH U)|)) . (LISTP SEXP W V U Z Y X CONS ADD1 LENGTH) . NIL . (LENGTH#3) . NIL . LENGTH . NIL . 3 .)(|∀U.LENGTH U=0≡NULL U| . (AXIOM (TM& . |∀U.LENGTH U=0≡NULL U|)) . (NULL LISTP SEXP W V U Z Y X CONS ADD1 LENGTH) . NIL . (LENGTH#4) . NIL . LENGTH . NIL . 4 .)(|∀U V.LENGTH (U*V)=LENGTH U+LENGTH V| . (AXIOM (TM& . |∀U V.LENGTH (U*V)=LENGTH U+LENGTH V|)) . (LISTP SEXP W V U Z Y X CONS APPEND ADD1 PLUS M N K J I LENGTH) . NIL . (LENGTH#5) . NIL . LENGTH . NIL . 5 .)(|∀X.LENGTH (X.NIL)=1| . (AXIOM (TM& . |∀X.LENGTH (X.NIL)=1|)) . (LISTP SEXP W V U Z Y X CONS ADD1 LENGTH) . NIL . (LENGTH#6) . NIL . LENGTH . NIL . 6 .)(|∀U N.LENGTH U≤N∨N<LENGTH U| . (AXIOM (TM& . |∀U N.LENGTH U≤N∨N<LENGTH U|)) . (LISTP SEXP W V U Z Y X CONS LESSP ADD1 M N K J I LESSEQ LENGTH) . NIL . (LENGTH#7) . NIL . LENGTH . NIL . 7 .)(|∀U Y.MEMBER(Y,U)⊃0<LENGTH U| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃0<LENGTH U|)) . (LISTP SEXP W V U Z Y X CONS MEMBER LESSP ADD1 LENGTH) . NIL . (LENGTH#8) . NIL . LENGTH . NIL . 8 .)(|∀U Y.MEMBER(Y,U)⊃¬NULL U| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃¬NULL U|)) . (NULL LISTP SEXP W V U Z Y X CONS MEMBER) . NIL . (LENGTH#9) . NIL . LENGTH . NIL . 9 .)(|∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)| . (AXIOM (TM& . |∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS MEMBER NTH) . NIL . (NTH#4) . NIL . NTH . NIL . 4 .)(|∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS MEMBER NTH) . NIL . (NTH#5) . NIL . NTH . NIL . 5 .)(|∀U.0<LENGTH U⊃NTH(U,0).NTHCDR(U,1)=U| . (AXIOM (TM& . |∀U.0<LENGTH U⊃NTH(U,0).NTHCDR(U,1)=U|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS NTH NTHCDR) . NIL . (NTHCDR#4) . NIL . NTHCDR . NIL . 4 .)(|∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)| . (AXIOM (TM& . |∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS NTH NTHCDR) . NIL . (NTHCDR#5) . NIL . NTHCDR . NIL . 5 .)(|∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')| . (AXIOM (TM& . |∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')|)) . (CDR LISTP SEXP ADD1 M N K J I W V U Z Y X CONS NTHCDR) . NIL . (NTHCDR#6) . NIL . NTHCDR . NIL . 6 .)(|∀U N.N<LENGTH U⊃NTHCDR(U,N)=NTH(U,N).NTHCDR(U,N')| . (AXIOM (TM& . |∀U N.N<LENGTH U⊃NTHCDR(U,N)=NTH(U,N).NTHCDR(U,N')|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS NTH NTHCDR) . NIL . (NTHCDR#7) . NIL . NTHCDR . NIL . 7 .)(|∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))| . (AXIOM (TM& . |∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS LESSEQ MEMBER NTH NTHCDR) . NIL . (NTHCDR#8) . NIL . NTHCDR . NIL . 8 .)(|∀U N M.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃NTH(NTHCDR(U,N),M)=NTH(U,M+N)| . (AXIOM (TM& . |∀U N M.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃NTH(NTHCDR(U,N),M)=NTH(U,M+N)|)) . (CAR LISTP SEXP LESSP ADD1 PLUS M N K J I LENGTH W V U Z Y X CONS NTH NTHCDR) . NIL . (NTHCDR#9) . NIL . NTHCDR . NIL . 9 .)(|∀U N.N≤LENGTH U⊃LENGTH (NTHCDR(U,N))=LENGTH U-N| . (AXIOM (TM& . |∀U N.N≤LENGTH U⊃LENGTH (NTHCDR(U,N))=LENGTH U-N|)) . (LISTP SEXP LESSP ADD1 M N K J I MINUS LENGTH W V U Z Y X CONS PRED LESSEQ NTHCDR) . NIL . (NTHCDR#10) . NIL . NTHCDR . NIL . 10 .)(|∀U.NTHCDR(U,LENGTH U)=NIL| . (AXIOM (TM& . |∀U.NTHCDR(U,LENGTH U)=NIL|)) . (LISTP SEXP ADD1 M N K J I LENGTH W V U Z Y X CONS NTHCDR) . NIL . (NTHCDR#11) . NIL . NTHCDR . NIL . 11 .)(|∀U N.LENGTH U≤N⊃NTHCDR(U,N)=NIL| . (AXIOM (TM& . |∀U N.LENGTH U≤N⊃NTHCDR(U,N)=NIL|)) . (LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS LESSEQ NTHCDR) . NIL . (NTHCDR#12) . NIL . NTHCDR . NIL . 12 .)(|∀A U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))| . (AXIOM (TM& . |∀A U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))|)) . (LISTP SEXP ADD1 M N K J I A W V U Z Y X PHI CONS ALLP A1 NTHCDR) . NIL . (NTHCDR#13) . NIL . NTHCDR . NIL . 13 .)(|∀PHI4 U.PHI4(NIL,LENGTH U)∧ (∀N.N<LENGTH U∧PHI4(NTHCDR(U,N'),N')⊃PHI4(NTH(U,N).NTHCDR(U,N'),N))⊃ PHI4(U,0)| . (AXIOM (TM& . |∀PHI4 U.PHI4(NIL,LENGTH U)∧ (∀N.N<LENGTH U∧PHI4(NTHCDR(U,N'),N')⊃PHI4(NTH(U,N).NTHCDR(U,N'),N))⊃ PHI4(U,0)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS NTH NTHCDR (PHI4 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NTHCDR#14 . NIL . VARIABLE .))) . NIL . (NTHCDR#14) . NIL . NTHCDR . NIL . 14 .)(|∀PHI U.PHI(NIL)∧ (∀N.N<LENGTH U⊃(PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N'))))⊃PHI(U)| . (AXIOM (TM& . |∀PHI U.PHI(NIL)∧ (∀N.N<LENGTH U⊃(PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N'))))⊃PHI(U)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X PHI CONS NTH NTHCDR) . NIL . (NTHCDR#15) . NIL . NTHCDR . NIL . 15 .)(|∀PHI1 U.(∀N.N<LENGTH U⊃PHI1(NTH(U,N)))⊃ALLP(PHI1,U)| . (AXIOM (TM& . |∀PHI1 U.(∀N.N<LENGTH U⊃PHI1(NTH(U,N)))⊃ALLP(PHI1,U)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X PHI CONS ALLP MEMBER PHI1 NTH) . NIL . (ALLP#6) . NIL . ALLP . NIL . 6 .)(|∀ALIST.LENGTH (DOM(ALIST))=LENGTH ALIST| . (AXIOM (TM& . |∀ALIST.LENGTH (DOM(ALIST))=LENGTH ALIST|)) . (ATOM LISTP ALISTP SEXP ADD1 LENGTH W V U Z Y X ZA YA XA CONS ALIST DOM) . NIL . (ALISTFACTS#3) . NIL . ALISTFACTS . NIL . 3 .)(|∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))| . (AXIOM (TM& . |∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))|)) . (ATOM LISTP ALISTP SEXP ADD1 LENGTH W V U Z Y X ZA YA XA CONS ALIST DOM RANGE) . NIL . (ALISTFACTS#4) . NIL . ALISTFACTS . NIL . 4 .)(|∀A N.(∀M.M<N⊃A(M))≡ALLNUM(N,A)| . (AXIOM (TM& . |∀A N.(∀M.M<N⊃A(M))≡ALLNUM(N,A)|)) . (LISTP SEXP LESSP ADD1 M N K J I SET A W V U Z Y X PHI CONS ALLP A1 ALLNUM) . NIL . (SUMFACTS#1) . NIL . SUMFACTS . NIL . 1 .)(|∀A N.(∃M.M<N∧A(M))≡SOMENUM(N,A)| . (AXIOM (TM& . |∀A N.(∃M.M<N∧A(M))≡SOMENUM(N,A)|)) . (LISTP SEXP LESSP ADD1 M N K J I SET A W V U Z Y X PHI CONS ALLP A1 SOMENUM) . NIL . (SUMFACTS#2) . NIL . SUMFACTS . NIL . 2 .)(|∀U A.NATNUM(MULT(U,A))| . (AXIOM (TM& . |∀U A.NATNUM(MULT(U,A))|)) . (LISTP SEXP ADD1 SET A W V U Z Y X PHI CONS ALLP A1 MULT) . NIL . (MULTIPLICITY#3) . NIL . MULTIPLICITY . NIL . 3 .)(|∀U A.MULT(U,A)≤LENGTH U| . (AXIOM (TM& . |∀U A.MULT(U,A)≤LENGTH U|)) . (LISTP SEXP LESSP ADD1 M N K J I SET A LENGTH W V U Z Y X PHI CONS LESSEQ ALLP A1 MULT) . NIL . (MULTIPLICITY#4) . NIL . MULTIPLICITY . NIL . 4 .)(|∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)| . (AXIOM (TM& . |∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)|)) . (LISTP SEXP LESSP ADD1 M N K J I SET A W V U Z Y X PHI CONS LESSEQ ALLP MEMBER A1 MULT) . NIL . (MULTIPLICITY#5) . NIL . MULTIPLICITY . NIL . 5 .)(|∀A U N.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)| . (AXIOM (TM& . |∀A U N.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)|)) . (LISTP SEXP LESSP ADD1 M N K J I SET A LENGTH NTHCDR W V U Z Y X PHI CONS LESSEQ ALLP A1 MULT) . NIL . (MULTIPLICITY#6) . NIL . MULTIPLICITY . NIL . 6 .)(|∀X U Y.FSTPOSITION(NIL,Y)=NIL∧ FSTPOSITION(X.U,Y)= (IF ¬MEMBER(Y,X.U) THEN NIL ELSE (IF X=Y THEN 0 ELSE FSTPOSITION(U,Y)'))| . (DEFINE FSTPOSITION (TM& . |∀X U Y.FSTPOSITION(NIL,Y)=NIL∧ FSTPOSITION(X.U,Y)= (IF ¬MEMBER(Y,X.U) THEN NIL ELSE (IF X=Y THEN 0 ELSE FSTPOSITION(U,Y)'))|) (USE (LR& LISPAX#34))) . ((FSTPOSITION . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FSTPOSITION#2 . NIL . DEFINED .)) LISTP SEXP ADD1 W V U Z Y X CONS MEMBER) . NIL . (FSTPOSITION#2 LISPAX#30 LISPAX#34 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3) . NIL . FSTPOSITION . NIL . 2 .)(|∀N SETSEQ.UN(SETSEQ,0)=EMPTYSET∧UN(SETSEQ,N')=UN(SETSEQ,N)∪SETSEQ(N)| . (DEFAX UN (TM& . |∀N SETSEQ.UN(SETSEQ,0)=EMPTYSET∧UN(SETSEQ,N')=UN(SETSEQ,N)∪SETSEQ(N)|)) . ((UN . (|((@SETSEQ)⊗(@N))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#10 . NIL . DEFINED .)) ZV YV XV URELEMENT BV AV ADD1 M N K J I SET UNION EMPTYSET SETSEQ) . NIL . (SUMS#10) . NIL . SUMS . NIL . 10 .)(NIL . (DECL DISJ_PAIR (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@SET)⊗(@SET))→TRUTHVAL|))) . ((DISJ_PAIR . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#11 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 11 .)(|∀U Y.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)|)) . (LISTP SEXP W V U Z Y X CONS MEMBER URELEMENT ZV YV XV BV AV INCLUSION MKSET MKLSET) . NIL . (SETFACTS#1) . NIL . SETFACTS . NIL . 1 .)(|∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV| . (AXIOM (TM& . |∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV INCLUSION) . NIL . (SETFACTS#2) . NIL . SETFACTS . NIL . 2 .)(|∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))| . (AXIOM (TM& . |∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))|)) . (CAR LISTP SEXP AV LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS MEMBER MKLSET NTH) . NIL . (SETFACTS#3) . NIL . SETFACTS . NIL . 3 .)(|∀U.MULT(U,EMPTYSET)=0| . (AXIOM (TM& . |∀U.MULT(U,EMPTYSET)=0|)) . (LISTP SEXP ZV YV XV URELEMENT ADD1 SET A W V U Z Y X PHI CONS ALLP A1 EMPTYSET MULT) . NIL . (MULTIPLICITY#7) . NIL . MULTIPLICITY . NIL . 7 .)(|∀V I J.I<J∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃2≤MULT(V,MKSET(NTH(V,I)))| . (AXIOM (TM& . |∀V I J.I<J∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃2≤MULT(V,MKSET(NTH(V,I)))|)) . (CAR LISTP SEXP ZV YV XV URELEMENT AV LESSP ADD1 M N K J I SET A LENGTH NTH W V U Z Y X PHI CONS LESSEQ ALLP A1 MKSET MULT) . NIL . (MULTIPLICITY#8) . NIL . MULTIPLICITY . NIL . 8 .)(|∀U Y.(NULL FSTPOSITION(U,Y)⊃¬MEMBER(Y,U))∧ (MEMBER(Y,U)⊃NATNUM(FSTPOSITION(U,Y)))∧ (NULL FSTPOSITION(U,Y)∨NATNUM(FSTPOSITION(U,Y)))| . (AXIOM (TM& . |∀U Y.(NULL FSTPOSITION(U,Y)⊃¬MEMBER(Y,U))∧ (MEMBER(Y,U)⊃NATNUM(FSTPOSITION(U,Y)))∧ (NULL FSTPOSITION(U,Y)∨NATNUM(FSTPOSITION(U,Y)))|)) . (NULL LISTP SEXP ADD1 W V U Z Y X CONS MEMBER FSTPOSITION) . NIL . (FSTPOSITION#3) . NIL . FSTPOSITION . NIL . 3 .)(|∀U Y.SEXP FSTPOSITION(U,Y)| . (AXIOM (TM& . |∀U Y.SEXP FSTPOSITION(U,Y)|)) . (LISTP SEXP ADD1 W V U Z Y X CONS MEMBER FSTPOSITION) . NIL . (FSTPOSITION#4) . NIL . FSTPOSITION . NIL . 4 .)(|∀U Y.MEMBER(Y,U)⊃FSTPOSITION(U,Y)<LENGTH U| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃FSTPOSITION(U,Y)<LENGTH U|)) . (LISTP SEXP LESSP ADD1 LENGTH W V U Z Y X CONS MEMBER FSTPOSITION) . NIL . (FSTPOSITION#5) . NIL . FSTPOSITION . NIL . 5 .)(|∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N| . (AXIOM (TM& . |∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N|)) . (CAR LISTP SEXP ADD1 M N K J I W V U Z Y X CONS MEMBER NTH FSTPOSITION) . NIL . (FSTPOSITION#6) . NIL . FSTPOSITION . NIL . 6 .)(|∀U N.UNIQUENESS(U)∧MEMBER(N,U)⊃FSTPOSITION(U,NTH(U,N))=N| . (AXIOM (TM& . |∀U N.UNIQUENESS(U)∧MEMBER(N,U)⊃FSTPOSITION(U,NTH(U,N))=N|)) . (CAR LISTP SEXP ADD1 M N K J I W V U Z Y X CONS MEMBER UNIQUENESS NTH FSTPOSITION) . NIL . (FSTPOSITION#7) . NIL . FSTPOSITION . NIL . 7 .)(|∀SETSEQ N M.M<N⊃SETSEQ(M)⊂UN(SETSEQ,N)| . (AXIOM (TM& . |∀SETSEQ N M.M<N⊃SETSEQ(M)⊂UN(SETSEQ,N)|)) . (ZV YV XV URELEMENT BV AV LESSP ADD1 M N K J I SET UNION INCLUSION EMPTYSET SETSEQ UN) . NIL . (SUMFACTS#3) . NIL . SUMFACTS . NIL . 3 .)(|∀U N.N≤LENGTH U⊃UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))| . (AXIOM (TM& . |∀U N.N≤LENGTH U⊃UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))|)) . (CAR LISTP SEXP ZV YV XV URELEMENT BV AV LESSP ADD1 M N K J I SET LENGTH NTH W V U Z Y X CONS LESSEQ UNION EMPTYSET MKSET SETSEQ UN) . NIL . (SUMFACTS#4) . NIL . SUMFACTS . NIL . 4 .)(|∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=(λX.(MKLSET(U))(X))| . (AXIOM (TM& . |∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=(λX.(MKLSET(U))(X))|)) . (CAR LISTP SEXP ZV YV XV URELEMENT BV AV ADD1 M N K J I SET LENGTH NTH W V U Z Y X CONS MEMBER UNION EMPTYSET MKSET MKLSET SETSEQ UN) . NIL . (SUMFACTS#5) . NIL . SUMFACTS . NIL . 5 .)(|∀NUMSEQ N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))| . (AXIOM (TM& . |∀NUMSEQ N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))|)) . (LESSP ADD1 M N K J I F NUMSEQ SUM) . NIL . (SUMFACTS#6) . NIL . SUMFACTS . NIL . 6 .)(|∀U.INJ(U)=(∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M)| . (DEFINE INJ (TM& . |∀U.INJ(U)=(∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M)|) NIL) . ((INJ . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INJ#2 . NIL . DEFINED .)) CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS NTH) . NIL . (INJ#2 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . INJ . NIL . 2 .)(|∀ALIST.FUNCTP(ALIST)≡UNIQUENESS(DOM(ALIST))| . (DEFINE FUNCTP (TM& . |∀ALIST.FUNCTP(ALIST)≡UNIQUENESS(DOM(ALIST))|) NIL) . ((FUNCTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#6 . NIL . DEFINED .)) ATOM LISTP ALISTP SEXP W V U Z Y X ZA YA XA CONS ALIST MEMBER UNIQUENESS DOM) . NIL . (APPALIST#6 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . APPALIST . NIL . 6 .)(NIL . (DECL INJECTP (TYPE: (TY& . GROUND→TRUTHVAL))) . ((INJECTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 7 .)(|∀U.UNIQUENESS(U)≡INJ(U)| . (AXIOM (TM& . |∀U.UNIQUENESS(U)≡INJ(U)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH W V U Z Y X CONS MEMBER UNIQUENESS NTH INJ) . NIL . (INJ#3) . NIL . INJ . NIL . 3 .)(|∀ALIST.INJECTP(ALIST)≡FUNCTP(ALIST)∧UNIQUENESS(RANGE(ALIST))| . (DEFINE INJECTP (TM& . |∀ALIST.INJECTP(ALIST)≡FUNCTP(ALIST)∧UNIQUENESS(RANGE(ALIST))|) NIL) . ((INJECTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#8 . NIL . DEFINED .)) ATOM LISTP ALISTP SEXP W V U Z Y X ZA YA XA CONS ALIST MEMBER UNIQUENESS DOM RANGE FUNCTP) . NIL . (APPALIST#8 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . APPALIST . NIL . 8 .)(NIL . (DECL (APPALIST) (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|))) . ((APPALIST . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#9 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 9 .)(|∀ALIST Y.APPALIST(Y,ALIST)=CDR ASSOC(Y,ALIST)| . (DEFINE APPALIST (TM& . |∀ALIST Y.APPALIST(Y,ALIST)=CDR ASSOC(Y,ALIST)|) NIL) . ((APPALIST . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#10 . NIL . DEFINED .)) CDR ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (APPALIST#10 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . APPALIST . NIL . 10 .)(NIL . (DECL (SAMEMAP) (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|))) . ((SAMEMAP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPALIST . NIL . 11 .)(|∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)| . (AXIOM (TM& . |∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)|)) . (CAR LISTP SEXP ZV YV XV URELEMENT AV LESSP ADD1 M N K J I SET A LENGTH NTH INJ W V U Z Y X PHI CONS ALLP A1 MKSET MULT) . NIL . (MULTIPLICITY#9) . NIL . MULTIPLICITY . NIL . 9 .)(|∀ALIST ALIST1.SAMEMAP(ALIST,ALIST1)≡ MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))∧ (∀Y.YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=APPALIST(Y,ALIST1))| . (DEFINE SAMEMAP (TM& . |∀ALIST ALIST1.SAMEMAP(ALIST,ALIST1)≡ MKLSET(DOM(ALIST))=MKLSET(DOM(ALIST1))∧ (∀Y.YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=APPALIST(Y,ALIST1))|) NIL) . ((SAMEMAP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#12 . NIL . DEFINED .)) CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST (ALIST1 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . ((BINDP& . 1000)) . APPALIST#12 . NIL . VARIABLE .))) . NIL . (APPALIST#12 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . APPALIST . NIL . 12 .)(|∀ALIST.PERMUTP(ALIST)≡FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))| . (DEFINE PERMUTP (TM& . |∀ALIST.PERMUTP(ALIST)≡FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))|) NIL) . ((PERMUTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPALIST#13 . NIL . DEFINED .)) ATOM LISTP ALISTP SEXP AV W V U Z Y X ZA YA XA CONS ALIST MEMBER UNIQUENESS MKLSET DOM RANGE FUNCTP) . NIL . (APPALIST#13 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4) . NIL . APPALIST . NIL . 13 .)(|∀CHI.CHI(NIL)∧(∀XA Y ALIST.CHI(ALIST)⊃CHI((XA.Y).ALIST))⊃(∀ALIST.CHI(ALIST))| . (AXIOM (TM& . |∀CHI.CHI(NIL)∧(∀XA Y ALIST.CHI(ALIST)⊃CHI((XA.Y).ALIST))⊃(∀ALIST.CHI(ALIST))|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST (CHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . APPALIST#14 . NIL . VARIABLE .))) . NIL . (APPALIST#14) . NIL . APPALIST . NIL . 14 .)(|∀ALIST Y.SEXP APPALIST(Y,ALIST)| . (AXIOM (TM& . |∀ALIST Y.SEXP APPALIST(Y,ALIST)|)) . (CDR ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC APPALIST) . NIL . (ALISTFACTS#5) . NIL . ALISTFACTS . NIL . 5 .)(|∀ALIST Y.¬YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=NIL| . (AXIOM (TM& . |∀ALIST Y.¬YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=NIL|)) . (CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST) . NIL . (ALISTFACTS#6) . NIL . ALISTFACTS . NIL . 6 .)(|∀ALIST.SAMEMAP(ALIST,ALIST)| . (AXIOM (TM& . |∀ALIST.SAMEMAP(ALIST,ALIST)|)) . (CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST SAMEMAP ALIST1) . NIL . (ALISTFACTS#7) . NIL . ALISTFACTS . NIL . 7 .)(|∀ALIST ALIST1.SAMEMAP(ALIST,ALIST1)⊃SAMEMAP(ALIST1,ALIST)| . (AXIOM (TM& . |∀ALIST ALIST1.SAMEMAP(ALIST,ALIST1)⊃SAMEMAP(ALIST1,ALIST)|)) . (CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST SAMEMAP ALIST1) . NIL . (ALISTFACTS#8) . NIL . ALISTFACTS . NIL . 8 .)(|∀ALIST ALIST1 ALIST2.SAMEMAP(ALIST,ALIST1)∧SAMEMAP(ALIST1,ALIST2)⊃ SAMEMAP(ALIST,ALIST2)| . (AXIOM (TM& . |∀ALIST ALIST1 ALIST2.SAMEMAP(ALIST,ALIST1)∧SAMEMAP(ALIST1,ALIST2)⊃ SAMEMAP(ALIST,ALIST2)|)) . (CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST SAMEMAP ALIST1 (ALIST2 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . ((BINDP& . 1000)) . ALISTFACTS#9 . NIL . VARIABLE .))) . NIL . (ALISTFACTS#9) . NIL . ALISTFACTS . NIL . 9 .)(|∀U I.APPL(U,I)=NTH(U,I)| . (DEFINE APPL (TM& . |∀U I.APPL(U,I)=NTH(U,I)|) NIL) . ((APPL . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#1 . NIL . DEFINED .)) CAR LISTP SEXP ADD1 M N K J I NTH W V U Z Y X CONS) . NIL . (APPL#1 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5) . NIL . APPL . NIL . 1 .)(|∀ALIST1 ALIST2.SAMEMAP(ALIST1,ALIST2)≡ MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧ (∀X.APPALIST(X,ALIST1)=APPALIST(X,ALIST2))| . (AXIOM (TM& . |∀ALIST1 ALIST2.SAMEMAP(ALIST1,ALIST2)≡ MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧ (∀X.APPALIST(X,ALIST1)=APPALIST(X,ALIST2))|)) . (CDR ATOM LISTP ALISTP SEXP ZV YV XV URELEMENT BV AV W V U Z Y X ZA YA XA CONS EPSILON ALIST ASSOC MEMBER MKLSET DOM APPALIST SAMEMAP ALIST1 ALIST2) . NIL . (ALISTFACTS#10) . NIL . ALISTFACTS . NIL . 10 .)(|∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V| . (AXIOM (TM& . |∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH NTH W V U Z Y X CONS APPL) . NIL . (APPL#2) . NIL . APPL . NIL . 2 .)(|∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)| . (AXIOM (TM& . |∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)|)) . (CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH NTH W V U Z Y X CONS MEMBER APPL) . NIL . (APPL#3) . NIL . APPL . NIL . 3 .)(NIL . (DECL (INTO) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((INTO . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPL . NIL . 4 .)(|∀A B.DISJ_PAIR(A,B)=EMPTYP(A∩B)| . (DEFINE DISJ_PAIR (TM& . |∀A B.DISJ_PAIR(A,B)=EMPTYP(A∩B)|) NIL) . ((DISJ_PAIR . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#12 . NIL . DEFINED .)) LISTP SEXP ZV YV XV URELEMENT BV AV SET C B A W V U Z Y X PHI CONS ALLP A1 INTERSECTION EMPTYP) . NIL . (SUMS#12 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5 APPL#3) . NIL . SUMS . NIL . 12 .)(NIL . (DECL DISJOINT (SYNTYPE: CONSTANT) (TYPE: (TY& . |((GROUND→(@SET))⊗GROUND)→TRUTHVAL|))) . ((DISJOINT . (|((GROUND→(@SET))⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#13 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . SUMS . NIL . 13 .)(|∀U.INTO(U)=(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)| . (DEFINE INTO (TM& . |∀U.INTO(U)=(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)|) NIL) . ((INTO . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#5 . NIL . DEFINED .)) CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH NTH W V U Z Y X CONS) . NIL . (APPL#5 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5 APPL#3) . NIL . APPL . NIL . 5 .)(NIL . (DECL (ONTO) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((ONTO . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPL . NIL . 6 .)(|∀N SETSEQ.DISJOINT(SETSEQ,0)∧ DISJOINT(SETSEQ,N')= (DISJOINT(SETSEQ,N)∧DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N)))| . (DEFAX DISJOINT (TM& . |∀N SETSEQ.DISJOINT(SETSEQ,0)∧ DISJOINT(SETSEQ,N')= (DISJOINT(SETSEQ,N)∧DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N)))|)) . ((DISJOINT . (|((GROUND→(@SET))⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SUMS#14 . NIL . DEFINED .)) LISTP SEXP ZV YV XV URELEMENT BV AV ADD1 M N K J I SET C B A W V U Z Y X PHI CONS ALLP A1 INTERSECTION UNION EMPTYSET EMPTYP SETSEQ UN DISJ_PAIR) . NIL . (SUMS#14) . NIL . SUMS . NIL . 14 .)(|∀U.ONTO(U)=(INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U)))| . (DEFINE ONTO (TM& . |∀U.ONTO(U)=(INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U)))|) NIL) . ((ONTO . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#7 . NIL . DEFINED .)) CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH NTH W V U Z Y X CONS MEMBER INTO) . NIL . (APPL#7 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5 APPL#3) . NIL . APPL . NIL . 7 .)(NIL . (DECL (PERM) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PERM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#8 . NIL . VARIABLE .))) . NIL . NIL . NIL . APPL . NIL . 8 .)(|∀U A B.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)| . (AXIOM (TM& . |∀U A B.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)|)) . (LISTP SEXP ZV YV XV URELEMENT BV AV ADD1 PLUS M N K J I SET C B A W V U Z Y X PHI CONS ALLP A1 INTERSECTION UNION EMPTYP DISJ_PAIR MULT) . NIL . (MULT_OF_UN_IS_SUM_UN#1) . NIL . MULT_OF_UN_IS_SUM_UN . NIL . 1 .)(|∀U.PERM(U)=ONTO(U)| . (DEFINE PERM (TM& . |∀U.PERM(U)=ONTO(U)|) NIL) . ((PERM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . APPL#9 . NIL . DEFINED .)) CAR LISTP SEXP LESSP ADD1 M N K J I LENGTH NTH W V U Z Y X CONS MEMBER INTO ONTO) . NIL . (APPL#9 LISPAX#34 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#17 NATNUM#9 NATNUM#13 NATNUM#14 NATNUM#16 LESSEQ#1 LESSEQ#4 LESSEQ#9 MINUS#3 MINUS#9 LENGTH#2 LENGTH#3 LENGTH#4 LENGTH#5 LENGTH#6 LENGTH#8 LENGTH#9 LISPAX#68 LISPAX#69 SETS#20 NTH#2 NTH#3 NTHCDR#2 NTHCDR#3 FSTPOSITION#3 FSTPOSITION#4 ALISTFACTS#1 ALISTFACTS#2 ALISTFACTS#5 APPL#3) . NIL . APPL . NIL . 9 .)(|∀SETSEQ U N.DISJOINT(SETSEQ,N)⊃ MULT(U,UN(SETSEQ,N))=SUM(λM.MULT(U,SETSEQ(M)),N)| . (AXIOM (TM& . |∀SETSEQ U N.DISJOINT(SETSEQ,N)⊃ MULT(U,UN(SETSEQ,N))=SUM(λM.MULT(U,SETSEQ(M)),N)|)) . (LISTP SEXP ZV YV XV URELEMENT BV AV ADD1 PLUS M N K J I SET C B A W V U Z Y X PHI CONS F NUMSEQ SUM SETSEQ UN ALLP A1 INTERSECTION UNION EMPTYSET EMPTYP DISJ_PAIR DISJOINT MULT) . NIL . (MULT_OF_UN_IS_SUM_UN#2) . NIL . MULT_OF_UN_IS_SUM_UN . NIL . 2 .)